Nuprl Definition : p-co-filter
11,40
postcript
pdf
p-co-filter(
f
)(
x
) == case
f
(
x
) of inl(
p
) => inr
p
| inr(
p
) => inl
x
latex
Definitions
x
.
A
(
x
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
f
(
a
)
,
inr
x
,
inl
x
FDL editor aliases
p-co-filter
origin
x.A(x)x.A(x)